Left Termination of the query pattern
myis(a,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 181 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 444 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES
    ↳28 PiDP
        ↳29 UsableRulesProof (⇔, 0 ms)
        ↳30 PiDP
        ↳31 PiDPToQDPProof (⇒, 0 ms)
        ↳32 QDP
        ↳33 QDPSizeChangeProof (⇔, 0 ms)
        ↳34 YES
    ↳35 PiDP
        ↳36 UsableRulesProof (⇔, 0 ms)
        ↳37 PiDP
        ↳38 PiDPToQDPProof (⇒, 0 ms)
        ↳39 QDP
        ↳40 QDPSizeChangeProof (⇔, 0 ms)
        ↳41 YES
    ↳42 PiDP
        ↳43 PiDPToQDPProof (⇒, 35 ms)
        ↳44 QDP
        ↳45 QDPSizeChangeProof (⇔, 0 ms)
        ↳46 YES

(0) Obligation:

Clauses:

myis(Z, X) :- evaluate(X, Z).
evaluate(+(X, Y), Z) :- ','(evaluate(X, X1), ','(evaluate(Y, Y1), add(X1, Y1, Z))).
evaluate(-(X, Y), Z) :- ','(evaluate(X, X1), ','(evaluate(Y, Y1), sub(X1, Y1, Z))).
evaluate(*(X, Y), Z) :- ','(evaluate(X, X1), ','(evaluate(Y, Y1), mult(X1, Y1, Z))).
evaluate(X, X) :- myinteger(X).
myinteger(s(X)) :- myinteger(X).
myinteger(0).
add(s(X), Y, s(Z)) :- add(X, Y, Z).
add(0, X, X).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).
mult(s(X), Y, R) :- ','(mult(X, Y, Z), add(Y, Z, R)).
mult(0, Y, 0).
notEq(s(X), s(Y)) :- notEq(X, Y).
notEq(s(X), 0).
notEq(0, s(X)).
lt(s(X), s(Y)) :- lt(X, Y).
lt(0, s(Y)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).

Query: myis(a,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

evaluateA(+(X1, X2), X3) :- evaluateA(X1, X4).
evaluateA(+(X1, X2), X3) :- ','(evaluatecA(X1, X4), evaluateA(X2, X5)).
evaluateA(+(X1, X2), X3) :- ','(evaluatecA(X1, X4), ','(evaluatecA(X2, X5), addB(X4, X5, X3))).
evaluateA(-(X1, X2), X3) :- evaluateA(X1, X4).
evaluateA(-(X1, X2), X3) :- ','(evaluatecA(X1, X4), evaluateA(X2, X5)).
evaluateA(-(X1, X2), X3) :- ','(evaluatecA(X1, X4), ','(evaluatecA(X2, X5), subC(X4, X5, X3))).
evaluateA(*(X1, X2), X3) :- evaluateA(X1, X4).
evaluateA(*(X1, X2), X3) :- ','(evaluatecA(X1, X4), evaluateA(X2, X5)).
evaluateA(*(X1, X2), X3) :- ','(evaluatecA(X1, s(X4)), ','(evaluatecA(X2, X5), multD(X4, X5, X6))).
evaluateA(*(X1, X2), X3) :- ','(evaluatecA(X1, s(X4)), ','(evaluatecA(X2, X5), ','(multcD(X4, X5, X6), addB(X5, X6, X3)))).
evaluateA(X1, X1) :- myintegerE(X1).
addB(s(X1), X2, s(X3)) :- addB(X1, X2, X3).
subC(s(X1), s(X2), X3) :- subC(X1, X2, X3).
multD(s(X1), X2, X3) :- multD(X1, X2, X4).
multD(s(X1), X2, X3) :- ','(multcD(X1, X2, X4), addF(X2, X4, X3)).
addF(s(X1), X2, s(X3)) :- addF(X1, X2, X3).
myintegerE(s(X1)) :- myintegerE(X1).
myisG(X1, X2) :- evaluateA(X2, X1).

Clauses:

evaluatecA(+(X1, X2), X3) :- ','(evaluatecA(X1, X4), ','(evaluatecA(X2, X5), addcB(X4, X5, X3))).
evaluatecA(-(X1, X2), X3) :- ','(evaluatecA(X1, X4), ','(evaluatecA(X2, X5), subcC(X4, X5, X3))).
evaluatecA(*(X1, X2), X3) :- ','(evaluatecA(X1, s(X4)), ','(evaluatecA(X2, X5), ','(multcD(X4, X5, X6), addcB(X5, X6, X3)))).
evaluatecA(*(X1, X2), 0) :- ','(evaluatecA(X1, 0), evaluatecA(X2, X3)).
evaluatecA(X1, X1) :- myintegercE(X1).
addcB(s(X1), X2, s(X3)) :- addcB(X1, X2, X3).
addcB(0, X1, X1).
subcC(s(X1), s(X2), X3) :- subcC(X1, X2, X3).
subcC(X1, 0, X1).
multcD(s(X1), X2, X3) :- ','(multcD(X1, X2, X4), addcF(X2, X4, X3)).
multcD(0, X1, 0).
addcF(s(X1), X2, s(X3)) :- addcF(X1, X2, X3).
addcF(0, X1, X1).
myintegercE(s(X1)) :- myintegercE(X1).
myintegercE(0).

Afs:

myisG(x1, x2)  =  myisG(x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
myisG_in: (f,b)
evaluateA_in: (b,f)
evaluatecA_in: (b,f) (b,b)
myintegercE_in: (b)
addcB_in: (b,b,b) (b,b,f)
subcC_in: (b,b,b) (b,b,f)
multcD_in: (b,b,f)
addcF_in: (b,b,f)
multD_in: (b,b,f)
addF_in: (b,b,f)
addB_in: (b,b,f)
myintegerE_in: (b)
subC_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

MYISG_IN_AG(X1, X2) → U27_AG(X1, X2, evaluateA_in_ga(X2, X1))
MYISG_IN_AG(X1, X2) → EVALUATEA_IN_GA(X2, X1)
EVALUATEA_IN_GA(+(X1, X2), X3) → U1_GA(X1, X2, X3, evaluateA_in_ga(X1, X4))
EVALUATEA_IN_GA(+(X1, X2), X3) → EVALUATEA_IN_GA(X1, X4)
EVALUATEA_IN_GA(+(X1, X2), X3) → U2_GA(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U2_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U3_GA(X1, X2, X3, evaluateA_in_ga(X2, X5))
U2_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2, X5)
EVALUATEA_IN_GA(-(X1, X2), X3) → U6_GA(X1, X2, X3, evaluateA_in_ga(X1, X4))
EVALUATEA_IN_GA(-(X1, X2), X3) → EVALUATEA_IN_GA(X1, X4)
EVALUATEA_IN_GA(-(X1, X2), X3) → U7_GA(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U7_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U8_GA(X1, X2, X3, evaluateA_in_ga(X2, X5))
U7_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2, X5)
EVALUATEA_IN_GA(*(X1, X2), X3) → U11_GA(X1, X2, X3, evaluateA_in_ga(X1, X4))
EVALUATEA_IN_GA(*(X1, X2), X3) → EVALUATEA_IN_GA(X1, X4)
EVALUATEA_IN_GA(*(X1, X2), X3) → U12_GA(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U12_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U13_GA(X1, X2, X3, evaluateA_in_ga(X2, X5))
U12_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2, X5)
EVALUATEA_IN_GA(*(X1, X2), X3) → U14_GA(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
U14_GA(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U15_GA(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U15_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U16_GA(X1, X2, X3, multD_in_gga(X4, X5, X6))
U15_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → MULTD_IN_GGA(X4, X5, X6)
MULTD_IN_GGA(s(X1), X2, X3) → U22_GGA(X1, X2, X3, multD_in_gga(X1, X2, X4))
MULTD_IN_GGA(s(X1), X2, X3) → MULTD_IN_GGA(X1, X2, X4)
MULTD_IN_GGA(s(X1), X2, X3) → U23_GGA(X1, X2, X3, multcD_in_gga(X1, X2, X4))
U23_GGA(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → U24_GGA(X1, X2, X3, addF_in_gga(X2, X4, X3))
U23_GGA(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → ADDF_IN_GGA(X2, X4, X3)
ADDF_IN_GGA(s(X1), X2, s(X3)) → U25_GGA(X1, X2, X3, addF_in_gga(X1, X2, X3))
ADDF_IN_GGA(s(X1), X2, s(X3)) → ADDF_IN_GGA(X1, X2, X3)
U15_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U17_GA(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
U17_GA(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U18_GA(X1, X2, X3, addB_in_gga(X5, X6, X3))
U17_GA(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → ADDB_IN_GGA(X5, X6, X3)
ADDB_IN_GGA(s(X1), X2, s(X3)) → U20_GGA(X1, X2, X3, addB_in_gga(X1, X2, X3))
ADDB_IN_GGA(s(X1), X2, s(X3)) → ADDB_IN_GGA(X1, X2, X3)
EVALUATEA_IN_GA(X1, X1) → U19_GA(X1, myintegerE_in_g(X1))
EVALUATEA_IN_GA(X1, X1) → MYINTEGERE_IN_G(X1)
MYINTEGERE_IN_G(s(X1)) → U26_G(X1, myintegerE_in_g(X1))
MYINTEGERE_IN_G(s(X1)) → MYINTEGERE_IN_G(X1)
U7_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U9_GA(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U9_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U10_GA(X1, X2, X3, subC_in_gga(X4, X5, X3))
U9_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → SUBC_IN_GGA(X4, X5, X3)
SUBC_IN_GGA(s(X1), s(X2), X3) → U21_GGA(X1, X2, X3, subC_in_gga(X1, X2, X3))
SUBC_IN_GGA(s(X1), s(X2), X3) → SUBC_IN_GGA(X1, X2, X3)
U2_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U4_GA(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U4_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U5_GA(X1, X2, X3, addB_in_gga(X4, X5, X3))
U4_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → ADDB_IN_GGA(X4, X5, X3)

The TRS R consists of the following rules:

evaluatecA_in_ga(+(X1, X2), X3) → U29_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(-(X1, X2), X3) → U32_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(*(X1, X2), X3) → U35_ga(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
evaluatecA_in_ga(*(X1, X2), 0) → U39_ga(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(+(X1, X2), X3) → U29_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(X1, X1) → U41_ga(X1, myintegercE_in_g(X1))
myintegercE_in_g(s(X1)) → U47_g(X1, myintegercE_in_g(X1))
myintegercE_in_g(0) → myintegercE_out_g(0)
U47_g(X1, myintegercE_out_g(X1)) → myintegercE_out_g(s(X1))
U41_ga(X1, myintegercE_out_g(X1)) → evaluatecA_out_ga(X1, X1)
U29_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_gg(X1, X2, X3, addcB_in_ggg(X4, X5, X3))
addcB_in_ggg(s(X1), X2, s(X3)) → U42_ggg(X1, X2, X3, addcB_in_ggg(X1, X2, X3))
addcB_in_ggg(0, X1, X1) → addcB_out_ggg(0, X1, X1)
U42_ggg(X1, X2, X3, addcB_out_ggg(X1, X2, X3)) → addcB_out_ggg(s(X1), X2, s(X3))
U31_gg(X1, X2, X3, addcB_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(+(X1, X2), X3)
evaluatecA_in_gg(-(X1, X2), X3) → U32_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U32_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_gg(X1, X2, X3, subcC_in_ggg(X4, X5, X3))
subcC_in_ggg(s(X1), s(X2), X3) → U43_ggg(X1, X2, X3, subcC_in_ggg(X1, X2, X3))
subcC_in_ggg(X1, 0, X1) → subcC_out_ggg(X1, 0, X1)
U43_ggg(X1, X2, X3, subcC_out_ggg(X1, X2, X3)) → subcC_out_ggg(s(X1), s(X2), X3)
U34_gg(X1, X2, X3, subcC_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(-(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), X3) → U35_gg(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
U35_gg(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_gg(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
multcD_in_gga(s(X1), X2, X3) → U44_gga(X1, X2, X3, multcD_in_gga(X1, X2, X4))
multcD_in_gga(0, X1, 0) → multcD_out_gga(0, X1, 0)
U44_gga(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → U45_gga(X1, X2, X3, addcF_in_gga(X2, X4, X3))
addcF_in_gga(s(X1), X2, s(X3)) → U46_gga(X1, X2, X3, addcF_in_gga(X1, X2, X3))
addcF_in_gga(0, X1, X1) → addcF_out_gga(0, X1, X1)
U46_gga(X1, X2, X3, addcF_out_gga(X1, X2, X3)) → addcF_out_gga(s(X1), X2, s(X3))
U45_gga(X1, X2, X3, addcF_out_gga(X2, X4, X3)) → multcD_out_gga(s(X1), X2, X3)
U37_gg(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_gg(X1, X2, X3, addcB_in_ggg(X5, X6, X3))
U38_gg(X1, X2, X3, addcB_out_ggg(X5, X6, X3)) → evaluatecA_out_gg(*(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), 0) → U39_gg(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(X1, X1) → U41_gg(X1, myintegercE_in_g(X1))
U41_gg(X1, myintegercE_out_g(X1)) → evaluatecA_out_gg(X1, X1)
U39_gg(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_gg(X1, X2, evaluatecA_in_ga(X2, X3))
U40_gg(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_gg(*(X1, X2), 0)
U39_ga(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_ga(X1, X2, evaluatecA_in_ga(X2, X3))
U40_ga(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_ga(*(X1, X2), 0)
U35_ga(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_ga(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
U37_ga(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_ga(X1, X2, X3, addcB_in_gga(X5, X6, X3))
addcB_in_gga(s(X1), X2, s(X3)) → U42_gga(X1, X2, X3, addcB_in_gga(X1, X2, X3))
addcB_in_gga(0, X1, X1) → addcB_out_gga(0, X1, X1)
U42_gga(X1, X2, X3, addcB_out_gga(X1, X2, X3)) → addcB_out_gga(s(X1), X2, s(X3))
U38_ga(X1, X2, X3, addcB_out_gga(X5, X6, X3)) → evaluatecA_out_ga(*(X1, X2), X3)
U32_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_ga(X1, X2, X3, subcC_in_gga(X4, X5, X3))
subcC_in_gga(s(X1), s(X2), X3) → U43_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U43_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
U34_ga(X1, X2, X3, subcC_out_gga(X4, X5, X3)) → evaluatecA_out_ga(-(X1, X2), X3)
U29_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_ga(X1, X2, X3, addcB_in_gga(X4, X5, X3))
U31_ga(X1, X2, X3, addcB_out_gga(X4, X5, X3)) → evaluatecA_out_ga(+(X1, X2), X3)

The argument filtering Pi contains the following mapping:
evaluateA_in_ga(x1, x2)  =  evaluateA_in_ga(x1)
+(x1, x2)  =  +(x1, x2)
evaluatecA_in_ga(x1, x2)  =  evaluatecA_in_ga(x1)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x1, x2, x4)
-(x1, x2)  =  -(x1, x2)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x1, x2, x4)
*(x1, x2)  =  *(x1, x2)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3)  =  U39_ga(x1, x2, x3)
evaluatecA_in_gg(x1, x2)  =  evaluatecA_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4)  =  U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2)  =  U41_ga(x1, x2)
myintegercE_in_g(x1)  =  myintegercE_in_g(x1)
s(x1)  =  s(x1)
U47_g(x1, x2)  =  U47_g(x1, x2)
0  =  0
myintegercE_out_g(x1)  =  myintegercE_out_g(x1)
evaluatecA_out_ga(x1, x2)  =  evaluatecA_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5)  =  U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4)  =  U31_gg(x1, x2, x3, x4)
addcB_in_ggg(x1, x2, x3)  =  addcB_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4)  =  U42_ggg(x1, x2, x3, x4)
addcB_out_ggg(x1, x2, x3)  =  addcB_out_ggg(x1, x2, x3)
evaluatecA_out_gg(x1, x2)  =  evaluatecA_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4)  =  U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5)  =  U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4)  =  U34_gg(x1, x2, x3, x4)
subcC_in_ggg(x1, x2, x3)  =  subcC_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4)  =  U43_ggg(x1, x2, x3, x4)
subcC_out_ggg(x1, x2, x3)  =  subcC_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4)  =  U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5)  =  U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5)  =  U37_gg(x1, x2, x3, x4, x5)
multcD_in_gga(x1, x2, x3)  =  multcD_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
multcD_out_gga(x1, x2, x3)  =  multcD_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
addcF_in_gga(x1, x2, x3)  =  addcF_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x1, x2, x4)
addcF_out_gga(x1, x2, x3)  =  addcF_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4)  =  U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
U41_gg(x1, x2)  =  U41_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5)  =  U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5)  =  U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x2, x4)
addcB_in_gga(x1, x2, x3)  =  addcB_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x1, x2, x4)
addcB_out_gga(x1, x2, x3)  =  addcB_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5)  =  U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4)  =  U34_ga(x1, x2, x4)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x1, x2, x4)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x1, x2, x4)
multD_in_gga(x1, x2, x3)  =  multD_in_gga(x1, x2)
addF_in_gga(x1, x2, x3)  =  addF_in_gga(x1, x2)
addB_in_gga(x1, x2, x3)  =  addB_in_gga(x1, x2)
myintegerE_in_g(x1)  =  myintegerE_in_g(x1)
subC_in_gga(x1, x2, x3)  =  subC_in_gga(x1, x2)
MYISG_IN_AG(x1, x2)  =  MYISG_IN_AG(x2)
U27_AG(x1, x2, x3)  =  U27_AG(x2, x3)
EVALUATEA_IN_GA(x1, x2)  =  EVALUATEA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x2, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x2, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x2, x4)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x2, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x2, x4)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x2, x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x2, x4)
U15_GA(x1, x2, x3, x4, x5)  =  U15_GA(x1, x2, x4, x5)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x1, x2, x4)
MULTD_IN_GGA(x1, x2, x3)  =  MULTD_IN_GGA(x1, x2)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
ADDF_IN_GGA(x1, x2, x3)  =  ADDF_IN_GGA(x1, x2)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
U17_GA(x1, x2, x3, x4, x5)  =  U17_GA(x1, x2, x4, x5)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x2, x4)
ADDB_IN_GGA(x1, x2, x3)  =  ADDB_IN_GGA(x1, x2)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x1, x2, x4)
U19_GA(x1, x2)  =  U19_GA(x1, x2)
MYINTEGERE_IN_G(x1)  =  MYINTEGERE_IN_G(x1)
U26_G(x1, x2)  =  U26_G(x1, x2)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x4, x5)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
SUBC_IN_GGA(x1, x2, x3)  =  SUBC_IN_GGA(x1, x2)
U21_GGA(x1, x2, x3, x4)  =  U21_GGA(x1, x2, x4)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x4, x5)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MYISG_IN_AG(X1, X2) → U27_AG(X1, X2, evaluateA_in_ga(X2, X1))
MYISG_IN_AG(X1, X2) → EVALUATEA_IN_GA(X2, X1)
EVALUATEA_IN_GA(+(X1, X2), X3) → U1_GA(X1, X2, X3, evaluateA_in_ga(X1, X4))
EVALUATEA_IN_GA(+(X1, X2), X3) → EVALUATEA_IN_GA(X1, X4)
EVALUATEA_IN_GA(+(X1, X2), X3) → U2_GA(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U2_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U3_GA(X1, X2, X3, evaluateA_in_ga(X2, X5))
U2_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2, X5)
EVALUATEA_IN_GA(-(X1, X2), X3) → U6_GA(X1, X2, X3, evaluateA_in_ga(X1, X4))
EVALUATEA_IN_GA(-(X1, X2), X3) → EVALUATEA_IN_GA(X1, X4)
EVALUATEA_IN_GA(-(X1, X2), X3) → U7_GA(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U7_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U8_GA(X1, X2, X3, evaluateA_in_ga(X2, X5))
U7_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2, X5)
EVALUATEA_IN_GA(*(X1, X2), X3) → U11_GA(X1, X2, X3, evaluateA_in_ga(X1, X4))
EVALUATEA_IN_GA(*(X1, X2), X3) → EVALUATEA_IN_GA(X1, X4)
EVALUATEA_IN_GA(*(X1, X2), X3) → U12_GA(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U12_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U13_GA(X1, X2, X3, evaluateA_in_ga(X2, X5))
U12_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2, X5)
EVALUATEA_IN_GA(*(X1, X2), X3) → U14_GA(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
U14_GA(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U15_GA(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U15_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U16_GA(X1, X2, X3, multD_in_gga(X4, X5, X6))
U15_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → MULTD_IN_GGA(X4, X5, X6)
MULTD_IN_GGA(s(X1), X2, X3) → U22_GGA(X1, X2, X3, multD_in_gga(X1, X2, X4))
MULTD_IN_GGA(s(X1), X2, X3) → MULTD_IN_GGA(X1, X2, X4)
MULTD_IN_GGA(s(X1), X2, X3) → U23_GGA(X1, X2, X3, multcD_in_gga(X1, X2, X4))
U23_GGA(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → U24_GGA(X1, X2, X3, addF_in_gga(X2, X4, X3))
U23_GGA(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → ADDF_IN_GGA(X2, X4, X3)
ADDF_IN_GGA(s(X1), X2, s(X3)) → U25_GGA(X1, X2, X3, addF_in_gga(X1, X2, X3))
ADDF_IN_GGA(s(X1), X2, s(X3)) → ADDF_IN_GGA(X1, X2, X3)
U15_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U17_GA(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
U17_GA(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U18_GA(X1, X2, X3, addB_in_gga(X5, X6, X3))
U17_GA(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → ADDB_IN_GGA(X5, X6, X3)
ADDB_IN_GGA(s(X1), X2, s(X3)) → U20_GGA(X1, X2, X3, addB_in_gga(X1, X2, X3))
ADDB_IN_GGA(s(X1), X2, s(X3)) → ADDB_IN_GGA(X1, X2, X3)
EVALUATEA_IN_GA(X1, X1) → U19_GA(X1, myintegerE_in_g(X1))
EVALUATEA_IN_GA(X1, X1) → MYINTEGERE_IN_G(X1)
MYINTEGERE_IN_G(s(X1)) → U26_G(X1, myintegerE_in_g(X1))
MYINTEGERE_IN_G(s(X1)) → MYINTEGERE_IN_G(X1)
U7_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U9_GA(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U9_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U10_GA(X1, X2, X3, subC_in_gga(X4, X5, X3))
U9_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → SUBC_IN_GGA(X4, X5, X3)
SUBC_IN_GGA(s(X1), s(X2), X3) → U21_GGA(X1, X2, X3, subC_in_gga(X1, X2, X3))
SUBC_IN_GGA(s(X1), s(X2), X3) → SUBC_IN_GGA(X1, X2, X3)
U2_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U4_GA(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U4_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U5_GA(X1, X2, X3, addB_in_gga(X4, X5, X3))
U4_GA(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → ADDB_IN_GGA(X4, X5, X3)

The TRS R consists of the following rules:

evaluatecA_in_ga(+(X1, X2), X3) → U29_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(-(X1, X2), X3) → U32_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(*(X1, X2), X3) → U35_ga(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
evaluatecA_in_ga(*(X1, X2), 0) → U39_ga(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(+(X1, X2), X3) → U29_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(X1, X1) → U41_ga(X1, myintegercE_in_g(X1))
myintegercE_in_g(s(X1)) → U47_g(X1, myintegercE_in_g(X1))
myintegercE_in_g(0) → myintegercE_out_g(0)
U47_g(X1, myintegercE_out_g(X1)) → myintegercE_out_g(s(X1))
U41_ga(X1, myintegercE_out_g(X1)) → evaluatecA_out_ga(X1, X1)
U29_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_gg(X1, X2, X3, addcB_in_ggg(X4, X5, X3))
addcB_in_ggg(s(X1), X2, s(X3)) → U42_ggg(X1, X2, X3, addcB_in_ggg(X1, X2, X3))
addcB_in_ggg(0, X1, X1) → addcB_out_ggg(0, X1, X1)
U42_ggg(X1, X2, X3, addcB_out_ggg(X1, X2, X3)) → addcB_out_ggg(s(X1), X2, s(X3))
U31_gg(X1, X2, X3, addcB_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(+(X1, X2), X3)
evaluatecA_in_gg(-(X1, X2), X3) → U32_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U32_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_gg(X1, X2, X3, subcC_in_ggg(X4, X5, X3))
subcC_in_ggg(s(X1), s(X2), X3) → U43_ggg(X1, X2, X3, subcC_in_ggg(X1, X2, X3))
subcC_in_ggg(X1, 0, X1) → subcC_out_ggg(X1, 0, X1)
U43_ggg(X1, X2, X3, subcC_out_ggg(X1, X2, X3)) → subcC_out_ggg(s(X1), s(X2), X3)
U34_gg(X1, X2, X3, subcC_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(-(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), X3) → U35_gg(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
U35_gg(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_gg(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
multcD_in_gga(s(X1), X2, X3) → U44_gga(X1, X2, X3, multcD_in_gga(X1, X2, X4))
multcD_in_gga(0, X1, 0) → multcD_out_gga(0, X1, 0)
U44_gga(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → U45_gga(X1, X2, X3, addcF_in_gga(X2, X4, X3))
addcF_in_gga(s(X1), X2, s(X3)) → U46_gga(X1, X2, X3, addcF_in_gga(X1, X2, X3))
addcF_in_gga(0, X1, X1) → addcF_out_gga(0, X1, X1)
U46_gga(X1, X2, X3, addcF_out_gga(X1, X2, X3)) → addcF_out_gga(s(X1), X2, s(X3))
U45_gga(X1, X2, X3, addcF_out_gga(X2, X4, X3)) → multcD_out_gga(s(X1), X2, X3)
U37_gg(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_gg(X1, X2, X3, addcB_in_ggg(X5, X6, X3))
U38_gg(X1, X2, X3, addcB_out_ggg(X5, X6, X3)) → evaluatecA_out_gg(*(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), 0) → U39_gg(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(X1, X1) → U41_gg(X1, myintegercE_in_g(X1))
U41_gg(X1, myintegercE_out_g(X1)) → evaluatecA_out_gg(X1, X1)
U39_gg(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_gg(X1, X2, evaluatecA_in_ga(X2, X3))
U40_gg(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_gg(*(X1, X2), 0)
U39_ga(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_ga(X1, X2, evaluatecA_in_ga(X2, X3))
U40_ga(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_ga(*(X1, X2), 0)
U35_ga(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_ga(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
U37_ga(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_ga(X1, X2, X3, addcB_in_gga(X5, X6, X3))
addcB_in_gga(s(X1), X2, s(X3)) → U42_gga(X1, X2, X3, addcB_in_gga(X1, X2, X3))
addcB_in_gga(0, X1, X1) → addcB_out_gga(0, X1, X1)
U42_gga(X1, X2, X3, addcB_out_gga(X1, X2, X3)) → addcB_out_gga(s(X1), X2, s(X3))
U38_ga(X1, X2, X3, addcB_out_gga(X5, X6, X3)) → evaluatecA_out_ga(*(X1, X2), X3)
U32_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_ga(X1, X2, X3, subcC_in_gga(X4, X5, X3))
subcC_in_gga(s(X1), s(X2), X3) → U43_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U43_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
U34_ga(X1, X2, X3, subcC_out_gga(X4, X5, X3)) → evaluatecA_out_ga(-(X1, X2), X3)
U29_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_ga(X1, X2, X3, addcB_in_gga(X4, X5, X3))
U31_ga(X1, X2, X3, addcB_out_gga(X4, X5, X3)) → evaluatecA_out_ga(+(X1, X2), X3)

The argument filtering Pi contains the following mapping:
evaluateA_in_ga(x1, x2)  =  evaluateA_in_ga(x1)
+(x1, x2)  =  +(x1, x2)
evaluatecA_in_ga(x1, x2)  =  evaluatecA_in_ga(x1)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x1, x2, x4)
-(x1, x2)  =  -(x1, x2)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x1, x2, x4)
*(x1, x2)  =  *(x1, x2)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3)  =  U39_ga(x1, x2, x3)
evaluatecA_in_gg(x1, x2)  =  evaluatecA_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4)  =  U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2)  =  U41_ga(x1, x2)
myintegercE_in_g(x1)  =  myintegercE_in_g(x1)
s(x1)  =  s(x1)
U47_g(x1, x2)  =  U47_g(x1, x2)
0  =  0
myintegercE_out_g(x1)  =  myintegercE_out_g(x1)
evaluatecA_out_ga(x1, x2)  =  evaluatecA_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5)  =  U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4)  =  U31_gg(x1, x2, x3, x4)
addcB_in_ggg(x1, x2, x3)  =  addcB_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4)  =  U42_ggg(x1, x2, x3, x4)
addcB_out_ggg(x1, x2, x3)  =  addcB_out_ggg(x1, x2, x3)
evaluatecA_out_gg(x1, x2)  =  evaluatecA_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4)  =  U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5)  =  U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4)  =  U34_gg(x1, x2, x3, x4)
subcC_in_ggg(x1, x2, x3)  =  subcC_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4)  =  U43_ggg(x1, x2, x3, x4)
subcC_out_ggg(x1, x2, x3)  =  subcC_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4)  =  U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5)  =  U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5)  =  U37_gg(x1, x2, x3, x4, x5)
multcD_in_gga(x1, x2, x3)  =  multcD_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
multcD_out_gga(x1, x2, x3)  =  multcD_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
addcF_in_gga(x1, x2, x3)  =  addcF_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x1, x2, x4)
addcF_out_gga(x1, x2, x3)  =  addcF_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4)  =  U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
U41_gg(x1, x2)  =  U41_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5)  =  U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5)  =  U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x2, x4)
addcB_in_gga(x1, x2, x3)  =  addcB_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x1, x2, x4)
addcB_out_gga(x1, x2, x3)  =  addcB_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5)  =  U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4)  =  U34_ga(x1, x2, x4)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x1, x2, x4)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x1, x2, x4)
multD_in_gga(x1, x2, x3)  =  multD_in_gga(x1, x2)
addF_in_gga(x1, x2, x3)  =  addF_in_gga(x1, x2)
addB_in_gga(x1, x2, x3)  =  addB_in_gga(x1, x2)
myintegerE_in_g(x1)  =  myintegerE_in_g(x1)
subC_in_gga(x1, x2, x3)  =  subC_in_gga(x1, x2)
MYISG_IN_AG(x1, x2)  =  MYISG_IN_AG(x2)
U27_AG(x1, x2, x3)  =  U27_AG(x2, x3)
EVALUATEA_IN_GA(x1, x2)  =  EVALUATEA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x2, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x2, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x2, x4)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x2, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x2, x4)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x2, x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x2, x4)
U15_GA(x1, x2, x3, x4, x5)  =  U15_GA(x1, x2, x4, x5)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x1, x2, x4)
MULTD_IN_GGA(x1, x2, x3)  =  MULTD_IN_GGA(x1, x2)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
ADDF_IN_GGA(x1, x2, x3)  =  ADDF_IN_GGA(x1, x2)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
U17_GA(x1, x2, x3, x4, x5)  =  U17_GA(x1, x2, x4, x5)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x2, x4)
ADDB_IN_GGA(x1, x2, x3)  =  ADDB_IN_GGA(x1, x2)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x1, x2, x4)
U19_GA(x1, x2)  =  U19_GA(x1, x2)
MYINTEGERE_IN_G(x1)  =  MYINTEGERE_IN_G(x1)
U26_G(x1, x2)  =  U26_G(x1, x2)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x4, x5)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
SUBC_IN_GGA(x1, x2, x3)  =  SUBC_IN_GGA(x1, x2)
U21_GGA(x1, x2, x3, x4)  =  U21_GGA(x1, x2, x4)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x4, x5)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 31 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBC_IN_GGA(s(X1), s(X2), X3) → SUBC_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

evaluatecA_in_ga(+(X1, X2), X3) → U29_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(-(X1, X2), X3) → U32_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(*(X1, X2), X3) → U35_ga(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
evaluatecA_in_ga(*(X1, X2), 0) → U39_ga(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(+(X1, X2), X3) → U29_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(X1, X1) → U41_ga(X1, myintegercE_in_g(X1))
myintegercE_in_g(s(X1)) → U47_g(X1, myintegercE_in_g(X1))
myintegercE_in_g(0) → myintegercE_out_g(0)
U47_g(X1, myintegercE_out_g(X1)) → myintegercE_out_g(s(X1))
U41_ga(X1, myintegercE_out_g(X1)) → evaluatecA_out_ga(X1, X1)
U29_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_gg(X1, X2, X3, addcB_in_ggg(X4, X5, X3))
addcB_in_ggg(s(X1), X2, s(X3)) → U42_ggg(X1, X2, X3, addcB_in_ggg(X1, X2, X3))
addcB_in_ggg(0, X1, X1) → addcB_out_ggg(0, X1, X1)
U42_ggg(X1, X2, X3, addcB_out_ggg(X1, X2, X3)) → addcB_out_ggg(s(X1), X2, s(X3))
U31_gg(X1, X2, X3, addcB_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(+(X1, X2), X3)
evaluatecA_in_gg(-(X1, X2), X3) → U32_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U32_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_gg(X1, X2, X3, subcC_in_ggg(X4, X5, X3))
subcC_in_ggg(s(X1), s(X2), X3) → U43_ggg(X1, X2, X3, subcC_in_ggg(X1, X2, X3))
subcC_in_ggg(X1, 0, X1) → subcC_out_ggg(X1, 0, X1)
U43_ggg(X1, X2, X3, subcC_out_ggg(X1, X2, X3)) → subcC_out_ggg(s(X1), s(X2), X3)
U34_gg(X1, X2, X3, subcC_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(-(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), X3) → U35_gg(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
U35_gg(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_gg(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
multcD_in_gga(s(X1), X2, X3) → U44_gga(X1, X2, X3, multcD_in_gga(X1, X2, X4))
multcD_in_gga(0, X1, 0) → multcD_out_gga(0, X1, 0)
U44_gga(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → U45_gga(X1, X2, X3, addcF_in_gga(X2, X4, X3))
addcF_in_gga(s(X1), X2, s(X3)) → U46_gga(X1, X2, X3, addcF_in_gga(X1, X2, X3))
addcF_in_gga(0, X1, X1) → addcF_out_gga(0, X1, X1)
U46_gga(X1, X2, X3, addcF_out_gga(X1, X2, X3)) → addcF_out_gga(s(X1), X2, s(X3))
U45_gga(X1, X2, X3, addcF_out_gga(X2, X4, X3)) → multcD_out_gga(s(X1), X2, X3)
U37_gg(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_gg(X1, X2, X3, addcB_in_ggg(X5, X6, X3))
U38_gg(X1, X2, X3, addcB_out_ggg(X5, X6, X3)) → evaluatecA_out_gg(*(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), 0) → U39_gg(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(X1, X1) → U41_gg(X1, myintegercE_in_g(X1))
U41_gg(X1, myintegercE_out_g(X1)) → evaluatecA_out_gg(X1, X1)
U39_gg(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_gg(X1, X2, evaluatecA_in_ga(X2, X3))
U40_gg(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_gg(*(X1, X2), 0)
U39_ga(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_ga(X1, X2, evaluatecA_in_ga(X2, X3))
U40_ga(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_ga(*(X1, X2), 0)
U35_ga(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_ga(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
U37_ga(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_ga(X1, X2, X3, addcB_in_gga(X5, X6, X3))
addcB_in_gga(s(X1), X2, s(X3)) → U42_gga(X1, X2, X3, addcB_in_gga(X1, X2, X3))
addcB_in_gga(0, X1, X1) → addcB_out_gga(0, X1, X1)
U42_gga(X1, X2, X3, addcB_out_gga(X1, X2, X3)) → addcB_out_gga(s(X1), X2, s(X3))
U38_ga(X1, X2, X3, addcB_out_gga(X5, X6, X3)) → evaluatecA_out_ga(*(X1, X2), X3)
U32_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_ga(X1, X2, X3, subcC_in_gga(X4, X5, X3))
subcC_in_gga(s(X1), s(X2), X3) → U43_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U43_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
U34_ga(X1, X2, X3, subcC_out_gga(X4, X5, X3)) → evaluatecA_out_ga(-(X1, X2), X3)
U29_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_ga(X1, X2, X3, addcB_in_gga(X4, X5, X3))
U31_ga(X1, X2, X3, addcB_out_gga(X4, X5, X3)) → evaluatecA_out_ga(+(X1, X2), X3)

The argument filtering Pi contains the following mapping:
+(x1, x2)  =  +(x1, x2)
evaluatecA_in_ga(x1, x2)  =  evaluatecA_in_ga(x1)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x1, x2, x4)
-(x1, x2)  =  -(x1, x2)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x1, x2, x4)
*(x1, x2)  =  *(x1, x2)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3)  =  U39_ga(x1, x2, x3)
evaluatecA_in_gg(x1, x2)  =  evaluatecA_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4)  =  U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2)  =  U41_ga(x1, x2)
myintegercE_in_g(x1)  =  myintegercE_in_g(x1)
s(x1)  =  s(x1)
U47_g(x1, x2)  =  U47_g(x1, x2)
0  =  0
myintegercE_out_g(x1)  =  myintegercE_out_g(x1)
evaluatecA_out_ga(x1, x2)  =  evaluatecA_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5)  =  U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4)  =  U31_gg(x1, x2, x3, x4)
addcB_in_ggg(x1, x2, x3)  =  addcB_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4)  =  U42_ggg(x1, x2, x3, x4)
addcB_out_ggg(x1, x2, x3)  =  addcB_out_ggg(x1, x2, x3)
evaluatecA_out_gg(x1, x2)  =  evaluatecA_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4)  =  U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5)  =  U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4)  =  U34_gg(x1, x2, x3, x4)
subcC_in_ggg(x1, x2, x3)  =  subcC_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4)  =  U43_ggg(x1, x2, x3, x4)
subcC_out_ggg(x1, x2, x3)  =  subcC_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4)  =  U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5)  =  U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5)  =  U37_gg(x1, x2, x3, x4, x5)
multcD_in_gga(x1, x2, x3)  =  multcD_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
multcD_out_gga(x1, x2, x3)  =  multcD_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
addcF_in_gga(x1, x2, x3)  =  addcF_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x1, x2, x4)
addcF_out_gga(x1, x2, x3)  =  addcF_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4)  =  U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
U41_gg(x1, x2)  =  U41_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5)  =  U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5)  =  U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x2, x4)
addcB_in_gga(x1, x2, x3)  =  addcB_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x1, x2, x4)
addcB_out_gga(x1, x2, x3)  =  addcB_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5)  =  U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4)  =  U34_ga(x1, x2, x4)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x1, x2, x4)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x1, x2, x4)
SUBC_IN_GGA(x1, x2, x3)  =  SUBC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBC_IN_GGA(s(X1), s(X2), X3) → SUBC_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUBC_IN_GGA(x1, x2, x3)  =  SUBC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUBC_IN_GGA(s(X1), s(X2)) → SUBC_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SUBC_IN_GGA(s(X1), s(X2)) → SUBC_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MYINTEGERE_IN_G(s(X1)) → MYINTEGERE_IN_G(X1)

The TRS R consists of the following rules:

evaluatecA_in_ga(+(X1, X2), X3) → U29_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(-(X1, X2), X3) → U32_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(*(X1, X2), X3) → U35_ga(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
evaluatecA_in_ga(*(X1, X2), 0) → U39_ga(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(+(X1, X2), X3) → U29_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(X1, X1) → U41_ga(X1, myintegercE_in_g(X1))
myintegercE_in_g(s(X1)) → U47_g(X1, myintegercE_in_g(X1))
myintegercE_in_g(0) → myintegercE_out_g(0)
U47_g(X1, myintegercE_out_g(X1)) → myintegercE_out_g(s(X1))
U41_ga(X1, myintegercE_out_g(X1)) → evaluatecA_out_ga(X1, X1)
U29_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_gg(X1, X2, X3, addcB_in_ggg(X4, X5, X3))
addcB_in_ggg(s(X1), X2, s(X3)) → U42_ggg(X1, X2, X3, addcB_in_ggg(X1, X2, X3))
addcB_in_ggg(0, X1, X1) → addcB_out_ggg(0, X1, X1)
U42_ggg(X1, X2, X3, addcB_out_ggg(X1, X2, X3)) → addcB_out_ggg(s(X1), X2, s(X3))
U31_gg(X1, X2, X3, addcB_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(+(X1, X2), X3)
evaluatecA_in_gg(-(X1, X2), X3) → U32_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U32_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_gg(X1, X2, X3, subcC_in_ggg(X4, X5, X3))
subcC_in_ggg(s(X1), s(X2), X3) → U43_ggg(X1, X2, X3, subcC_in_ggg(X1, X2, X3))
subcC_in_ggg(X1, 0, X1) → subcC_out_ggg(X1, 0, X1)
U43_ggg(X1, X2, X3, subcC_out_ggg(X1, X2, X3)) → subcC_out_ggg(s(X1), s(X2), X3)
U34_gg(X1, X2, X3, subcC_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(-(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), X3) → U35_gg(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
U35_gg(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_gg(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
multcD_in_gga(s(X1), X2, X3) → U44_gga(X1, X2, X3, multcD_in_gga(X1, X2, X4))
multcD_in_gga(0, X1, 0) → multcD_out_gga(0, X1, 0)
U44_gga(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → U45_gga(X1, X2, X3, addcF_in_gga(X2, X4, X3))
addcF_in_gga(s(X1), X2, s(X3)) → U46_gga(X1, X2, X3, addcF_in_gga(X1, X2, X3))
addcF_in_gga(0, X1, X1) → addcF_out_gga(0, X1, X1)
U46_gga(X1, X2, X3, addcF_out_gga(X1, X2, X3)) → addcF_out_gga(s(X1), X2, s(X3))
U45_gga(X1, X2, X3, addcF_out_gga(X2, X4, X3)) → multcD_out_gga(s(X1), X2, X3)
U37_gg(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_gg(X1, X2, X3, addcB_in_ggg(X5, X6, X3))
U38_gg(X1, X2, X3, addcB_out_ggg(X5, X6, X3)) → evaluatecA_out_gg(*(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), 0) → U39_gg(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(X1, X1) → U41_gg(X1, myintegercE_in_g(X1))
U41_gg(X1, myintegercE_out_g(X1)) → evaluatecA_out_gg(X1, X1)
U39_gg(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_gg(X1, X2, evaluatecA_in_ga(X2, X3))
U40_gg(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_gg(*(X1, X2), 0)
U39_ga(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_ga(X1, X2, evaluatecA_in_ga(X2, X3))
U40_ga(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_ga(*(X1, X2), 0)
U35_ga(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_ga(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
U37_ga(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_ga(X1, X2, X3, addcB_in_gga(X5, X6, X3))
addcB_in_gga(s(X1), X2, s(X3)) → U42_gga(X1, X2, X3, addcB_in_gga(X1, X2, X3))
addcB_in_gga(0, X1, X1) → addcB_out_gga(0, X1, X1)
U42_gga(X1, X2, X3, addcB_out_gga(X1, X2, X3)) → addcB_out_gga(s(X1), X2, s(X3))
U38_ga(X1, X2, X3, addcB_out_gga(X5, X6, X3)) → evaluatecA_out_ga(*(X1, X2), X3)
U32_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_ga(X1, X2, X3, subcC_in_gga(X4, X5, X3))
subcC_in_gga(s(X1), s(X2), X3) → U43_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U43_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
U34_ga(X1, X2, X3, subcC_out_gga(X4, X5, X3)) → evaluatecA_out_ga(-(X1, X2), X3)
U29_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_ga(X1, X2, X3, addcB_in_gga(X4, X5, X3))
U31_ga(X1, X2, X3, addcB_out_gga(X4, X5, X3)) → evaluatecA_out_ga(+(X1, X2), X3)

The argument filtering Pi contains the following mapping:
+(x1, x2)  =  +(x1, x2)
evaluatecA_in_ga(x1, x2)  =  evaluatecA_in_ga(x1)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x1, x2, x4)
-(x1, x2)  =  -(x1, x2)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x1, x2, x4)
*(x1, x2)  =  *(x1, x2)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3)  =  U39_ga(x1, x2, x3)
evaluatecA_in_gg(x1, x2)  =  evaluatecA_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4)  =  U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2)  =  U41_ga(x1, x2)
myintegercE_in_g(x1)  =  myintegercE_in_g(x1)
s(x1)  =  s(x1)
U47_g(x1, x2)  =  U47_g(x1, x2)
0  =  0
myintegercE_out_g(x1)  =  myintegercE_out_g(x1)
evaluatecA_out_ga(x1, x2)  =  evaluatecA_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5)  =  U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4)  =  U31_gg(x1, x2, x3, x4)
addcB_in_ggg(x1, x2, x3)  =  addcB_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4)  =  U42_ggg(x1, x2, x3, x4)
addcB_out_ggg(x1, x2, x3)  =  addcB_out_ggg(x1, x2, x3)
evaluatecA_out_gg(x1, x2)  =  evaluatecA_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4)  =  U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5)  =  U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4)  =  U34_gg(x1, x2, x3, x4)
subcC_in_ggg(x1, x2, x3)  =  subcC_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4)  =  U43_ggg(x1, x2, x3, x4)
subcC_out_ggg(x1, x2, x3)  =  subcC_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4)  =  U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5)  =  U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5)  =  U37_gg(x1, x2, x3, x4, x5)
multcD_in_gga(x1, x2, x3)  =  multcD_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
multcD_out_gga(x1, x2, x3)  =  multcD_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
addcF_in_gga(x1, x2, x3)  =  addcF_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x1, x2, x4)
addcF_out_gga(x1, x2, x3)  =  addcF_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4)  =  U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
U41_gg(x1, x2)  =  U41_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5)  =  U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5)  =  U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x2, x4)
addcB_in_gga(x1, x2, x3)  =  addcB_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x1, x2, x4)
addcB_out_gga(x1, x2, x3)  =  addcB_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5)  =  U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4)  =  U34_ga(x1, x2, x4)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x1, x2, x4)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x1, x2, x4)
MYINTEGERE_IN_G(x1)  =  MYINTEGERE_IN_G(x1)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MYINTEGERE_IN_G(s(X1)) → MYINTEGERE_IN_G(X1)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MYINTEGERE_IN_G(s(X1)) → MYINTEGERE_IN_G(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MYINTEGERE_IN_G(s(X1)) → MYINTEGERE_IN_G(X1)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDB_IN_GGA(s(X1), X2, s(X3)) → ADDB_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

evaluatecA_in_ga(+(X1, X2), X3) → U29_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(-(X1, X2), X3) → U32_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(*(X1, X2), X3) → U35_ga(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
evaluatecA_in_ga(*(X1, X2), 0) → U39_ga(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(+(X1, X2), X3) → U29_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(X1, X1) → U41_ga(X1, myintegercE_in_g(X1))
myintegercE_in_g(s(X1)) → U47_g(X1, myintegercE_in_g(X1))
myintegercE_in_g(0) → myintegercE_out_g(0)
U47_g(X1, myintegercE_out_g(X1)) → myintegercE_out_g(s(X1))
U41_ga(X1, myintegercE_out_g(X1)) → evaluatecA_out_ga(X1, X1)
U29_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_gg(X1, X2, X3, addcB_in_ggg(X4, X5, X3))
addcB_in_ggg(s(X1), X2, s(X3)) → U42_ggg(X1, X2, X3, addcB_in_ggg(X1, X2, X3))
addcB_in_ggg(0, X1, X1) → addcB_out_ggg(0, X1, X1)
U42_ggg(X1, X2, X3, addcB_out_ggg(X1, X2, X3)) → addcB_out_ggg(s(X1), X2, s(X3))
U31_gg(X1, X2, X3, addcB_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(+(X1, X2), X3)
evaluatecA_in_gg(-(X1, X2), X3) → U32_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U32_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_gg(X1, X2, X3, subcC_in_ggg(X4, X5, X3))
subcC_in_ggg(s(X1), s(X2), X3) → U43_ggg(X1, X2, X3, subcC_in_ggg(X1, X2, X3))
subcC_in_ggg(X1, 0, X1) → subcC_out_ggg(X1, 0, X1)
U43_ggg(X1, X2, X3, subcC_out_ggg(X1, X2, X3)) → subcC_out_ggg(s(X1), s(X2), X3)
U34_gg(X1, X2, X3, subcC_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(-(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), X3) → U35_gg(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
U35_gg(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_gg(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
multcD_in_gga(s(X1), X2, X3) → U44_gga(X1, X2, X3, multcD_in_gga(X1, X2, X4))
multcD_in_gga(0, X1, 0) → multcD_out_gga(0, X1, 0)
U44_gga(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → U45_gga(X1, X2, X3, addcF_in_gga(X2, X4, X3))
addcF_in_gga(s(X1), X2, s(X3)) → U46_gga(X1, X2, X3, addcF_in_gga(X1, X2, X3))
addcF_in_gga(0, X1, X1) → addcF_out_gga(0, X1, X1)
U46_gga(X1, X2, X3, addcF_out_gga(X1, X2, X3)) → addcF_out_gga(s(X1), X2, s(X3))
U45_gga(X1, X2, X3, addcF_out_gga(X2, X4, X3)) → multcD_out_gga(s(X1), X2, X3)
U37_gg(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_gg(X1, X2, X3, addcB_in_ggg(X5, X6, X3))
U38_gg(X1, X2, X3, addcB_out_ggg(X5, X6, X3)) → evaluatecA_out_gg(*(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), 0) → U39_gg(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(X1, X1) → U41_gg(X1, myintegercE_in_g(X1))
U41_gg(X1, myintegercE_out_g(X1)) → evaluatecA_out_gg(X1, X1)
U39_gg(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_gg(X1, X2, evaluatecA_in_ga(X2, X3))
U40_gg(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_gg(*(X1, X2), 0)
U39_ga(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_ga(X1, X2, evaluatecA_in_ga(X2, X3))
U40_ga(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_ga(*(X1, X2), 0)
U35_ga(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_ga(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
U37_ga(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_ga(X1, X2, X3, addcB_in_gga(X5, X6, X3))
addcB_in_gga(s(X1), X2, s(X3)) → U42_gga(X1, X2, X3, addcB_in_gga(X1, X2, X3))
addcB_in_gga(0, X1, X1) → addcB_out_gga(0, X1, X1)
U42_gga(X1, X2, X3, addcB_out_gga(X1, X2, X3)) → addcB_out_gga(s(X1), X2, s(X3))
U38_ga(X1, X2, X3, addcB_out_gga(X5, X6, X3)) → evaluatecA_out_ga(*(X1, X2), X3)
U32_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_ga(X1, X2, X3, subcC_in_gga(X4, X5, X3))
subcC_in_gga(s(X1), s(X2), X3) → U43_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U43_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
U34_ga(X1, X2, X3, subcC_out_gga(X4, X5, X3)) → evaluatecA_out_ga(-(X1, X2), X3)
U29_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_ga(X1, X2, X3, addcB_in_gga(X4, X5, X3))
U31_ga(X1, X2, X3, addcB_out_gga(X4, X5, X3)) → evaluatecA_out_ga(+(X1, X2), X3)

The argument filtering Pi contains the following mapping:
+(x1, x2)  =  +(x1, x2)
evaluatecA_in_ga(x1, x2)  =  evaluatecA_in_ga(x1)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x1, x2, x4)
-(x1, x2)  =  -(x1, x2)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x1, x2, x4)
*(x1, x2)  =  *(x1, x2)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3)  =  U39_ga(x1, x2, x3)
evaluatecA_in_gg(x1, x2)  =  evaluatecA_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4)  =  U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2)  =  U41_ga(x1, x2)
myintegercE_in_g(x1)  =  myintegercE_in_g(x1)
s(x1)  =  s(x1)
U47_g(x1, x2)  =  U47_g(x1, x2)
0  =  0
myintegercE_out_g(x1)  =  myintegercE_out_g(x1)
evaluatecA_out_ga(x1, x2)  =  evaluatecA_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5)  =  U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4)  =  U31_gg(x1, x2, x3, x4)
addcB_in_ggg(x1, x2, x3)  =  addcB_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4)  =  U42_ggg(x1, x2, x3, x4)
addcB_out_ggg(x1, x2, x3)  =  addcB_out_ggg(x1, x2, x3)
evaluatecA_out_gg(x1, x2)  =  evaluatecA_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4)  =  U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5)  =  U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4)  =  U34_gg(x1, x2, x3, x4)
subcC_in_ggg(x1, x2, x3)  =  subcC_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4)  =  U43_ggg(x1, x2, x3, x4)
subcC_out_ggg(x1, x2, x3)  =  subcC_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4)  =  U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5)  =  U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5)  =  U37_gg(x1, x2, x3, x4, x5)
multcD_in_gga(x1, x2, x3)  =  multcD_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
multcD_out_gga(x1, x2, x3)  =  multcD_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
addcF_in_gga(x1, x2, x3)  =  addcF_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x1, x2, x4)
addcF_out_gga(x1, x2, x3)  =  addcF_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4)  =  U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
U41_gg(x1, x2)  =  U41_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5)  =  U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5)  =  U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x2, x4)
addcB_in_gga(x1, x2, x3)  =  addcB_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x1, x2, x4)
addcB_out_gga(x1, x2, x3)  =  addcB_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5)  =  U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4)  =  U34_ga(x1, x2, x4)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x1, x2, x4)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x1, x2, x4)
ADDB_IN_GGA(x1, x2, x3)  =  ADDB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDB_IN_GGA(s(X1), X2, s(X3)) → ADDB_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ADDB_IN_GGA(x1, x2, x3)  =  ADDB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ADDB_IN_GGA(s(X1), X2) → ADDB_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ADDB_IN_GGA(s(X1), X2) → ADDB_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDF_IN_GGA(s(X1), X2, s(X3)) → ADDF_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

evaluatecA_in_ga(+(X1, X2), X3) → U29_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(-(X1, X2), X3) → U32_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(*(X1, X2), X3) → U35_ga(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
evaluatecA_in_ga(*(X1, X2), 0) → U39_ga(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(+(X1, X2), X3) → U29_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(X1, X1) → U41_ga(X1, myintegercE_in_g(X1))
myintegercE_in_g(s(X1)) → U47_g(X1, myintegercE_in_g(X1))
myintegercE_in_g(0) → myintegercE_out_g(0)
U47_g(X1, myintegercE_out_g(X1)) → myintegercE_out_g(s(X1))
U41_ga(X1, myintegercE_out_g(X1)) → evaluatecA_out_ga(X1, X1)
U29_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_gg(X1, X2, X3, addcB_in_ggg(X4, X5, X3))
addcB_in_ggg(s(X1), X2, s(X3)) → U42_ggg(X1, X2, X3, addcB_in_ggg(X1, X2, X3))
addcB_in_ggg(0, X1, X1) → addcB_out_ggg(0, X1, X1)
U42_ggg(X1, X2, X3, addcB_out_ggg(X1, X2, X3)) → addcB_out_ggg(s(X1), X2, s(X3))
U31_gg(X1, X2, X3, addcB_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(+(X1, X2), X3)
evaluatecA_in_gg(-(X1, X2), X3) → U32_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U32_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_gg(X1, X2, X3, subcC_in_ggg(X4, X5, X3))
subcC_in_ggg(s(X1), s(X2), X3) → U43_ggg(X1, X2, X3, subcC_in_ggg(X1, X2, X3))
subcC_in_ggg(X1, 0, X1) → subcC_out_ggg(X1, 0, X1)
U43_ggg(X1, X2, X3, subcC_out_ggg(X1, X2, X3)) → subcC_out_ggg(s(X1), s(X2), X3)
U34_gg(X1, X2, X3, subcC_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(-(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), X3) → U35_gg(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
U35_gg(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_gg(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
multcD_in_gga(s(X1), X2, X3) → U44_gga(X1, X2, X3, multcD_in_gga(X1, X2, X4))
multcD_in_gga(0, X1, 0) → multcD_out_gga(0, X1, 0)
U44_gga(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → U45_gga(X1, X2, X3, addcF_in_gga(X2, X4, X3))
addcF_in_gga(s(X1), X2, s(X3)) → U46_gga(X1, X2, X3, addcF_in_gga(X1, X2, X3))
addcF_in_gga(0, X1, X1) → addcF_out_gga(0, X1, X1)
U46_gga(X1, X2, X3, addcF_out_gga(X1, X2, X3)) → addcF_out_gga(s(X1), X2, s(X3))
U45_gga(X1, X2, X3, addcF_out_gga(X2, X4, X3)) → multcD_out_gga(s(X1), X2, X3)
U37_gg(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_gg(X1, X2, X3, addcB_in_ggg(X5, X6, X3))
U38_gg(X1, X2, X3, addcB_out_ggg(X5, X6, X3)) → evaluatecA_out_gg(*(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), 0) → U39_gg(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(X1, X1) → U41_gg(X1, myintegercE_in_g(X1))
U41_gg(X1, myintegercE_out_g(X1)) → evaluatecA_out_gg(X1, X1)
U39_gg(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_gg(X1, X2, evaluatecA_in_ga(X2, X3))
U40_gg(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_gg(*(X1, X2), 0)
U39_ga(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_ga(X1, X2, evaluatecA_in_ga(X2, X3))
U40_ga(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_ga(*(X1, X2), 0)
U35_ga(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_ga(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
U37_ga(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_ga(X1, X2, X3, addcB_in_gga(X5, X6, X3))
addcB_in_gga(s(X1), X2, s(X3)) → U42_gga(X1, X2, X3, addcB_in_gga(X1, X2, X3))
addcB_in_gga(0, X1, X1) → addcB_out_gga(0, X1, X1)
U42_gga(X1, X2, X3, addcB_out_gga(X1, X2, X3)) → addcB_out_gga(s(X1), X2, s(X3))
U38_ga(X1, X2, X3, addcB_out_gga(X5, X6, X3)) → evaluatecA_out_ga(*(X1, X2), X3)
U32_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_ga(X1, X2, X3, subcC_in_gga(X4, X5, X3))
subcC_in_gga(s(X1), s(X2), X3) → U43_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U43_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
U34_ga(X1, X2, X3, subcC_out_gga(X4, X5, X3)) → evaluatecA_out_ga(-(X1, X2), X3)
U29_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_ga(X1, X2, X3, addcB_in_gga(X4, X5, X3))
U31_ga(X1, X2, X3, addcB_out_gga(X4, X5, X3)) → evaluatecA_out_ga(+(X1, X2), X3)

The argument filtering Pi contains the following mapping:
+(x1, x2)  =  +(x1, x2)
evaluatecA_in_ga(x1, x2)  =  evaluatecA_in_ga(x1)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x1, x2, x4)
-(x1, x2)  =  -(x1, x2)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x1, x2, x4)
*(x1, x2)  =  *(x1, x2)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3)  =  U39_ga(x1, x2, x3)
evaluatecA_in_gg(x1, x2)  =  evaluatecA_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4)  =  U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2)  =  U41_ga(x1, x2)
myintegercE_in_g(x1)  =  myintegercE_in_g(x1)
s(x1)  =  s(x1)
U47_g(x1, x2)  =  U47_g(x1, x2)
0  =  0
myintegercE_out_g(x1)  =  myintegercE_out_g(x1)
evaluatecA_out_ga(x1, x2)  =  evaluatecA_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5)  =  U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4)  =  U31_gg(x1, x2, x3, x4)
addcB_in_ggg(x1, x2, x3)  =  addcB_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4)  =  U42_ggg(x1, x2, x3, x4)
addcB_out_ggg(x1, x2, x3)  =  addcB_out_ggg(x1, x2, x3)
evaluatecA_out_gg(x1, x2)  =  evaluatecA_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4)  =  U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5)  =  U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4)  =  U34_gg(x1, x2, x3, x4)
subcC_in_ggg(x1, x2, x3)  =  subcC_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4)  =  U43_ggg(x1, x2, x3, x4)
subcC_out_ggg(x1, x2, x3)  =  subcC_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4)  =  U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5)  =  U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5)  =  U37_gg(x1, x2, x3, x4, x5)
multcD_in_gga(x1, x2, x3)  =  multcD_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
multcD_out_gga(x1, x2, x3)  =  multcD_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
addcF_in_gga(x1, x2, x3)  =  addcF_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x1, x2, x4)
addcF_out_gga(x1, x2, x3)  =  addcF_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4)  =  U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
U41_gg(x1, x2)  =  U41_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5)  =  U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5)  =  U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x2, x4)
addcB_in_gga(x1, x2, x3)  =  addcB_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x1, x2, x4)
addcB_out_gga(x1, x2, x3)  =  addcB_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5)  =  U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4)  =  U34_ga(x1, x2, x4)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x1, x2, x4)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x1, x2, x4)
ADDF_IN_GGA(x1, x2, x3)  =  ADDF_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDF_IN_GGA(s(X1), X2, s(X3)) → ADDF_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ADDF_IN_GGA(x1, x2, x3)  =  ADDF_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ADDF_IN_GGA(s(X1), X2) → ADDF_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ADDF_IN_GGA(s(X1), X2) → ADDF_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTD_IN_GGA(s(X1), X2, X3) → MULTD_IN_GGA(X1, X2, X4)

The TRS R consists of the following rules:

evaluatecA_in_ga(+(X1, X2), X3) → U29_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(-(X1, X2), X3) → U32_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(*(X1, X2), X3) → U35_ga(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
evaluatecA_in_ga(*(X1, X2), 0) → U39_ga(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(+(X1, X2), X3) → U29_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(X1, X1) → U41_ga(X1, myintegercE_in_g(X1))
myintegercE_in_g(s(X1)) → U47_g(X1, myintegercE_in_g(X1))
myintegercE_in_g(0) → myintegercE_out_g(0)
U47_g(X1, myintegercE_out_g(X1)) → myintegercE_out_g(s(X1))
U41_ga(X1, myintegercE_out_g(X1)) → evaluatecA_out_ga(X1, X1)
U29_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_gg(X1, X2, X3, addcB_in_ggg(X4, X5, X3))
addcB_in_ggg(s(X1), X2, s(X3)) → U42_ggg(X1, X2, X3, addcB_in_ggg(X1, X2, X3))
addcB_in_ggg(0, X1, X1) → addcB_out_ggg(0, X1, X1)
U42_ggg(X1, X2, X3, addcB_out_ggg(X1, X2, X3)) → addcB_out_ggg(s(X1), X2, s(X3))
U31_gg(X1, X2, X3, addcB_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(+(X1, X2), X3)
evaluatecA_in_gg(-(X1, X2), X3) → U32_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U32_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_gg(X1, X2, X3, subcC_in_ggg(X4, X5, X3))
subcC_in_ggg(s(X1), s(X2), X3) → U43_ggg(X1, X2, X3, subcC_in_ggg(X1, X2, X3))
subcC_in_ggg(X1, 0, X1) → subcC_out_ggg(X1, 0, X1)
U43_ggg(X1, X2, X3, subcC_out_ggg(X1, X2, X3)) → subcC_out_ggg(s(X1), s(X2), X3)
U34_gg(X1, X2, X3, subcC_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(-(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), X3) → U35_gg(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
U35_gg(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_gg(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
multcD_in_gga(s(X1), X2, X3) → U44_gga(X1, X2, X3, multcD_in_gga(X1, X2, X4))
multcD_in_gga(0, X1, 0) → multcD_out_gga(0, X1, 0)
U44_gga(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → U45_gga(X1, X2, X3, addcF_in_gga(X2, X4, X3))
addcF_in_gga(s(X1), X2, s(X3)) → U46_gga(X1, X2, X3, addcF_in_gga(X1, X2, X3))
addcF_in_gga(0, X1, X1) → addcF_out_gga(0, X1, X1)
U46_gga(X1, X2, X3, addcF_out_gga(X1, X2, X3)) → addcF_out_gga(s(X1), X2, s(X3))
U45_gga(X1, X2, X3, addcF_out_gga(X2, X4, X3)) → multcD_out_gga(s(X1), X2, X3)
U37_gg(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_gg(X1, X2, X3, addcB_in_ggg(X5, X6, X3))
U38_gg(X1, X2, X3, addcB_out_ggg(X5, X6, X3)) → evaluatecA_out_gg(*(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), 0) → U39_gg(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(X1, X1) → U41_gg(X1, myintegercE_in_g(X1))
U41_gg(X1, myintegercE_out_g(X1)) → evaluatecA_out_gg(X1, X1)
U39_gg(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_gg(X1, X2, evaluatecA_in_ga(X2, X3))
U40_gg(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_gg(*(X1, X2), 0)
U39_ga(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_ga(X1, X2, evaluatecA_in_ga(X2, X3))
U40_ga(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_ga(*(X1, X2), 0)
U35_ga(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_ga(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
U37_ga(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_ga(X1, X2, X3, addcB_in_gga(X5, X6, X3))
addcB_in_gga(s(X1), X2, s(X3)) → U42_gga(X1, X2, X3, addcB_in_gga(X1, X2, X3))
addcB_in_gga(0, X1, X1) → addcB_out_gga(0, X1, X1)
U42_gga(X1, X2, X3, addcB_out_gga(X1, X2, X3)) → addcB_out_gga(s(X1), X2, s(X3))
U38_ga(X1, X2, X3, addcB_out_gga(X5, X6, X3)) → evaluatecA_out_ga(*(X1, X2), X3)
U32_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_ga(X1, X2, X3, subcC_in_gga(X4, X5, X3))
subcC_in_gga(s(X1), s(X2), X3) → U43_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U43_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
U34_ga(X1, X2, X3, subcC_out_gga(X4, X5, X3)) → evaluatecA_out_ga(-(X1, X2), X3)
U29_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_ga(X1, X2, X3, addcB_in_gga(X4, X5, X3))
U31_ga(X1, X2, X3, addcB_out_gga(X4, X5, X3)) → evaluatecA_out_ga(+(X1, X2), X3)

The argument filtering Pi contains the following mapping:
+(x1, x2)  =  +(x1, x2)
evaluatecA_in_ga(x1, x2)  =  evaluatecA_in_ga(x1)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x1, x2, x4)
-(x1, x2)  =  -(x1, x2)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x1, x2, x4)
*(x1, x2)  =  *(x1, x2)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3)  =  U39_ga(x1, x2, x3)
evaluatecA_in_gg(x1, x2)  =  evaluatecA_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4)  =  U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2)  =  U41_ga(x1, x2)
myintegercE_in_g(x1)  =  myintegercE_in_g(x1)
s(x1)  =  s(x1)
U47_g(x1, x2)  =  U47_g(x1, x2)
0  =  0
myintegercE_out_g(x1)  =  myintegercE_out_g(x1)
evaluatecA_out_ga(x1, x2)  =  evaluatecA_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5)  =  U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4)  =  U31_gg(x1, x2, x3, x4)
addcB_in_ggg(x1, x2, x3)  =  addcB_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4)  =  U42_ggg(x1, x2, x3, x4)
addcB_out_ggg(x1, x2, x3)  =  addcB_out_ggg(x1, x2, x3)
evaluatecA_out_gg(x1, x2)  =  evaluatecA_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4)  =  U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5)  =  U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4)  =  U34_gg(x1, x2, x3, x4)
subcC_in_ggg(x1, x2, x3)  =  subcC_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4)  =  U43_ggg(x1, x2, x3, x4)
subcC_out_ggg(x1, x2, x3)  =  subcC_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4)  =  U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5)  =  U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5)  =  U37_gg(x1, x2, x3, x4, x5)
multcD_in_gga(x1, x2, x3)  =  multcD_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
multcD_out_gga(x1, x2, x3)  =  multcD_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
addcF_in_gga(x1, x2, x3)  =  addcF_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x1, x2, x4)
addcF_out_gga(x1, x2, x3)  =  addcF_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4)  =  U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
U41_gg(x1, x2)  =  U41_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5)  =  U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5)  =  U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x2, x4)
addcB_in_gga(x1, x2, x3)  =  addcB_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x1, x2, x4)
addcB_out_gga(x1, x2, x3)  =  addcB_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5)  =  U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4)  =  U34_ga(x1, x2, x4)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x1, x2, x4)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x1, x2, x4)
MULTD_IN_GGA(x1, x2, x3)  =  MULTD_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTD_IN_GGA(s(X1), X2, X3) → MULTD_IN_GGA(X1, X2, X4)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTD_IN_GGA(x1, x2, x3)  =  MULTD_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTD_IN_GGA(s(X1), X2) → MULTD_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTD_IN_GGA(s(X1), X2) → MULTD_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

(41) YES

(42) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

EVALUATEA_IN_GA(+(X1, X2), X3) → U2_GA(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U2_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2, X5)
EVALUATEA_IN_GA(+(X1, X2), X3) → EVALUATEA_IN_GA(X1, X4)
EVALUATEA_IN_GA(-(X1, X2), X3) → EVALUATEA_IN_GA(X1, X4)
EVALUATEA_IN_GA(-(X1, X2), X3) → U7_GA(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U7_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2, X5)
EVALUATEA_IN_GA(*(X1, X2), X3) → EVALUATEA_IN_GA(X1, X4)
EVALUATEA_IN_GA(*(X1, X2), X3) → U12_GA(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U12_GA(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2, X5)

The TRS R consists of the following rules:

evaluatecA_in_ga(+(X1, X2), X3) → U29_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(-(X1, X2), X3) → U32_ga(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(*(X1, X2), X3) → U35_ga(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
evaluatecA_in_ga(*(X1, X2), 0) → U39_ga(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(+(X1, X2), X3) → U29_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
evaluatecA_in_ga(X1, X1) → U41_ga(X1, myintegercE_in_g(X1))
myintegercE_in_g(s(X1)) → U47_g(X1, myintegercE_in_g(X1))
myintegercE_in_g(0) → myintegercE_out_g(0)
U47_g(X1, myintegercE_out_g(X1)) → myintegercE_out_g(s(X1))
U41_ga(X1, myintegercE_out_g(X1)) → evaluatecA_out_ga(X1, X1)
U29_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_gg(X1, X2, X3, addcB_in_ggg(X4, X5, X3))
addcB_in_ggg(s(X1), X2, s(X3)) → U42_ggg(X1, X2, X3, addcB_in_ggg(X1, X2, X3))
addcB_in_ggg(0, X1, X1) → addcB_out_ggg(0, X1, X1)
U42_ggg(X1, X2, X3, addcB_out_ggg(X1, X2, X3)) → addcB_out_ggg(s(X1), X2, s(X3))
U31_gg(X1, X2, X3, addcB_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(+(X1, X2), X3)
evaluatecA_in_gg(-(X1, X2), X3) → U32_gg(X1, X2, X3, evaluatecA_in_ga(X1, X4))
U32_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_gg(X1, X2, X3, subcC_in_ggg(X4, X5, X3))
subcC_in_ggg(s(X1), s(X2), X3) → U43_ggg(X1, X2, X3, subcC_in_ggg(X1, X2, X3))
subcC_in_ggg(X1, 0, X1) → subcC_out_ggg(X1, 0, X1)
U43_ggg(X1, X2, X3, subcC_out_ggg(X1, X2, X3)) → subcC_out_ggg(s(X1), s(X2), X3)
U34_gg(X1, X2, X3, subcC_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(-(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), X3) → U35_gg(X1, X2, X3, evaluatecA_in_ga(X1, s(X4)))
U35_gg(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_gg(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
multcD_in_gga(s(X1), X2, X3) → U44_gga(X1, X2, X3, multcD_in_gga(X1, X2, X4))
multcD_in_gga(0, X1, 0) → multcD_out_gga(0, X1, 0)
U44_gga(X1, X2, X3, multcD_out_gga(X1, X2, X4)) → U45_gga(X1, X2, X3, addcF_in_gga(X2, X4, X3))
addcF_in_gga(s(X1), X2, s(X3)) → U46_gga(X1, X2, X3, addcF_in_gga(X1, X2, X3))
addcF_in_gga(0, X1, X1) → addcF_out_gga(0, X1, X1)
U46_gga(X1, X2, X3, addcF_out_gga(X1, X2, X3)) → addcF_out_gga(s(X1), X2, s(X3))
U45_gga(X1, X2, X3, addcF_out_gga(X2, X4, X3)) → multcD_out_gga(s(X1), X2, X3)
U37_gg(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_gg(X1, X2, X3, addcB_in_ggg(X5, X6, X3))
U38_gg(X1, X2, X3, addcB_out_ggg(X5, X6, X3)) → evaluatecA_out_gg(*(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), 0) → U39_gg(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(X1, X1) → U41_gg(X1, myintegercE_in_g(X1))
U41_gg(X1, myintegercE_out_g(X1)) → evaluatecA_out_gg(X1, X1)
U39_gg(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_gg(X1, X2, evaluatecA_in_ga(X2, X3))
U40_gg(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_gg(*(X1, X2), 0)
U39_ga(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_ga(X1, X2, evaluatecA_in_ga(X2, X3))
U40_ga(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_ga(*(X1, X2), 0)
U35_ga(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U36_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_ga(X1, X2, X3, X5, multcD_in_gga(X4, X5, X6))
U37_ga(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_ga(X1, X2, X3, addcB_in_gga(X5, X6, X3))
addcB_in_gga(s(X1), X2, s(X3)) → U42_gga(X1, X2, X3, addcB_in_gga(X1, X2, X3))
addcB_in_gga(0, X1, X1) → addcB_out_gga(0, X1, X1)
U42_gga(X1, X2, X3, addcB_out_gga(X1, X2, X3)) → addcB_out_gga(s(X1), X2, s(X3))
U38_ga(X1, X2, X3, addcB_out_gga(X5, X6, X3)) → evaluatecA_out_ga(*(X1, X2), X3)
U32_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U33_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_ga(X1, X2, X3, subcC_in_gga(X4, X5, X3))
subcC_in_gga(s(X1), s(X2), X3) → U43_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U43_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
U34_ga(X1, X2, X3, subcC_out_gga(X4, X5, X3)) → evaluatecA_out_ga(-(X1, X2), X3)
U29_ga(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_ga(X1, X2, X3, X4, evaluatecA_in_ga(X2, X5))
U30_ga(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_ga(X1, X2, X3, addcB_in_gga(X4, X5, X3))
U31_ga(X1, X2, X3, addcB_out_gga(X4, X5, X3)) → evaluatecA_out_ga(+(X1, X2), X3)

The argument filtering Pi contains the following mapping:
+(x1, x2)  =  +(x1, x2)
evaluatecA_in_ga(x1, x2)  =  evaluatecA_in_ga(x1)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x1, x2, x4)
-(x1, x2)  =  -(x1, x2)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x1, x2, x4)
*(x1, x2)  =  *(x1, x2)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3)  =  U39_ga(x1, x2, x3)
evaluatecA_in_gg(x1, x2)  =  evaluatecA_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4)  =  U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2)  =  U41_ga(x1, x2)
myintegercE_in_g(x1)  =  myintegercE_in_g(x1)
s(x1)  =  s(x1)
U47_g(x1, x2)  =  U47_g(x1, x2)
0  =  0
myintegercE_out_g(x1)  =  myintegercE_out_g(x1)
evaluatecA_out_ga(x1, x2)  =  evaluatecA_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5)  =  U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4)  =  U31_gg(x1, x2, x3, x4)
addcB_in_ggg(x1, x2, x3)  =  addcB_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4)  =  U42_ggg(x1, x2, x3, x4)
addcB_out_ggg(x1, x2, x3)  =  addcB_out_ggg(x1, x2, x3)
evaluatecA_out_gg(x1, x2)  =  evaluatecA_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4)  =  U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5)  =  U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4)  =  U34_gg(x1, x2, x3, x4)
subcC_in_ggg(x1, x2, x3)  =  subcC_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4)  =  U43_ggg(x1, x2, x3, x4)
subcC_out_ggg(x1, x2, x3)  =  subcC_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4)  =  U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5)  =  U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5)  =  U37_gg(x1, x2, x3, x4, x5)
multcD_in_gga(x1, x2, x3)  =  multcD_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
multcD_out_gga(x1, x2, x3)  =  multcD_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
addcF_in_gga(x1, x2, x3)  =  addcF_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x1, x2, x4)
addcF_out_gga(x1, x2, x3)  =  addcF_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4)  =  U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
U41_gg(x1, x2)  =  U41_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5)  =  U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5)  =  U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x2, x4)
addcB_in_gga(x1, x2, x3)  =  addcB_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x1, x2, x4)
addcB_out_gga(x1, x2, x3)  =  addcB_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5)  =  U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4)  =  U34_ga(x1, x2, x4)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x1, x2, x4)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x1, x2, x4)
EVALUATEA_IN_GA(x1, x2)  =  EVALUATEA_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x2, x4)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(43) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

EVALUATEA_IN_GA(+(X1, X2)) → U2_GA(X1, X2, evaluatecA_in_ga(X1))
U2_GA(X1, X2, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2)
EVALUATEA_IN_GA(+(X1, X2)) → EVALUATEA_IN_GA(X1)
EVALUATEA_IN_GA(-(X1, X2)) → EVALUATEA_IN_GA(X1)
EVALUATEA_IN_GA(-(X1, X2)) → U7_GA(X1, X2, evaluatecA_in_ga(X1))
U7_GA(X1, X2, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2)
EVALUATEA_IN_GA(*(X1, X2)) → EVALUATEA_IN_GA(X1)
EVALUATEA_IN_GA(*(X1, X2)) → U12_GA(X1, X2, evaluatecA_in_ga(X1))
U12_GA(X1, X2, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2)

The TRS R consists of the following rules:

evaluatecA_in_ga(+(X1, X2)) → U29_ga(X1, X2, evaluatecA_in_ga(X1))
evaluatecA_in_ga(-(X1, X2)) → U32_ga(X1, X2, evaluatecA_in_ga(X1))
evaluatecA_in_ga(*(X1, X2)) → U35_ga(X1, X2, evaluatecA_in_ga(X1))
evaluatecA_in_ga(*(X1, X2)) → U39_ga(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(+(X1, X2), X3) → U29_gg(X1, X2, X3, evaluatecA_in_ga(X1))
evaluatecA_in_ga(X1) → U41_ga(X1, myintegercE_in_g(X1))
myintegercE_in_g(s(X1)) → U47_g(X1, myintegercE_in_g(X1))
myintegercE_in_g(0) → myintegercE_out_g(0)
U47_g(X1, myintegercE_out_g(X1)) → myintegercE_out_g(s(X1))
U41_ga(X1, myintegercE_out_g(X1)) → evaluatecA_out_ga(X1, X1)
U29_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U30_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2))
U30_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U31_gg(X1, X2, X3, addcB_in_ggg(X4, X5, X3))
addcB_in_ggg(s(X1), X2, s(X3)) → U42_ggg(X1, X2, X3, addcB_in_ggg(X1, X2, X3))
addcB_in_ggg(0, X1, X1) → addcB_out_ggg(0, X1, X1)
U42_ggg(X1, X2, X3, addcB_out_ggg(X1, X2, X3)) → addcB_out_ggg(s(X1), X2, s(X3))
U31_gg(X1, X2, X3, addcB_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(+(X1, X2), X3)
evaluatecA_in_gg(-(X1, X2), X3) → U32_gg(X1, X2, X3, evaluatecA_in_ga(X1))
U32_gg(X1, X2, X3, evaluatecA_out_ga(X1, X4)) → U33_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2))
U33_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U34_gg(X1, X2, X3, subcC_in_ggg(X4, X5, X3))
subcC_in_ggg(s(X1), s(X2), X3) → U43_ggg(X1, X2, X3, subcC_in_ggg(X1, X2, X3))
subcC_in_ggg(X1, 0, X1) → subcC_out_ggg(X1, 0, X1)
U43_ggg(X1, X2, X3, subcC_out_ggg(X1, X2, X3)) → subcC_out_ggg(s(X1), s(X2), X3)
U34_gg(X1, X2, X3, subcC_out_ggg(X4, X5, X3)) → evaluatecA_out_gg(-(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), X3) → U35_gg(X1, X2, X3, evaluatecA_in_ga(X1))
U35_gg(X1, X2, X3, evaluatecA_out_ga(X1, s(X4))) → U36_gg(X1, X2, X3, X4, evaluatecA_in_ga(X2))
U36_gg(X1, X2, X3, X4, evaluatecA_out_ga(X2, X5)) → U37_gg(X1, X2, X3, X5, multcD_in_gga(X4, X5))
multcD_in_gga(s(X1), X2) → U44_gga(X1, X2, multcD_in_gga(X1, X2))
multcD_in_gga(0, X1) → multcD_out_gga(0, X1, 0)
U44_gga(X1, X2, multcD_out_gga(X1, X2, X4)) → U45_gga(X1, X2, addcF_in_gga(X2, X4))
addcF_in_gga(s(X1), X2) → U46_gga(X1, X2, addcF_in_gga(X1, X2))
addcF_in_gga(0, X1) → addcF_out_gga(0, X1, X1)
U46_gga(X1, X2, addcF_out_gga(X1, X2, X3)) → addcF_out_gga(s(X1), X2, s(X3))
U45_gga(X1, X2, addcF_out_gga(X2, X4, X3)) → multcD_out_gga(s(X1), X2, X3)
U37_gg(X1, X2, X3, X5, multcD_out_gga(X4, X5, X6)) → U38_gg(X1, X2, X3, addcB_in_ggg(X5, X6, X3))
U38_gg(X1, X2, X3, addcB_out_ggg(X5, X6, X3)) → evaluatecA_out_gg(*(X1, X2), X3)
evaluatecA_in_gg(*(X1, X2), 0) → U39_gg(X1, X2, evaluatecA_in_gg(X1, 0))
evaluatecA_in_gg(X1, X1) → U41_gg(X1, myintegercE_in_g(X1))
U41_gg(X1, myintegercE_out_g(X1)) → evaluatecA_out_gg(X1, X1)
U39_gg(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_gg(X1, X2, evaluatecA_in_ga(X2))
U40_gg(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_gg(*(X1, X2), 0)
U39_ga(X1, X2, evaluatecA_out_gg(X1, 0)) → U40_ga(X1, X2, evaluatecA_in_ga(X2))
U40_ga(X1, X2, evaluatecA_out_ga(X2, X3)) → evaluatecA_out_ga(*(X1, X2), 0)
U35_ga(X1, X2, evaluatecA_out_ga(X1, s(X4))) → U36_ga(X1, X2, X4, evaluatecA_in_ga(X2))
U36_ga(X1, X2, X4, evaluatecA_out_ga(X2, X5)) → U37_ga(X1, X2, X5, multcD_in_gga(X4, X5))
U37_ga(X1, X2, X5, multcD_out_gga(X4, X5, X6)) → U38_ga(X1, X2, addcB_in_gga(X5, X6))
addcB_in_gga(s(X1), X2) → U42_gga(X1, X2, addcB_in_gga(X1, X2))
addcB_in_gga(0, X1) → addcB_out_gga(0, X1, X1)
U42_gga(X1, X2, addcB_out_gga(X1, X2, X3)) → addcB_out_gga(s(X1), X2, s(X3))
U38_ga(X1, X2, addcB_out_gga(X5, X6, X3)) → evaluatecA_out_ga(*(X1, X2), X3)
U32_ga(X1, X2, evaluatecA_out_ga(X1, X4)) → U33_ga(X1, X2, X4, evaluatecA_in_ga(X2))
U33_ga(X1, X2, X4, evaluatecA_out_ga(X2, X5)) → U34_ga(X1, X2, subcC_in_gga(X4, X5))
subcC_in_gga(s(X1), s(X2)) → U43_gga(X1, X2, subcC_in_gga(X1, X2))
subcC_in_gga(X1, 0) → subcC_out_gga(X1, 0, X1)
U43_gga(X1, X2, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
U34_ga(X1, X2, subcC_out_gga(X4, X5, X3)) → evaluatecA_out_ga(-(X1, X2), X3)
U29_ga(X1, X2, evaluatecA_out_ga(X1, X4)) → U30_ga(X1, X2, X4, evaluatecA_in_ga(X2))
U30_ga(X1, X2, X4, evaluatecA_out_ga(X2, X5)) → U31_ga(X1, X2, addcB_in_gga(X4, X5))
U31_ga(X1, X2, addcB_out_gga(X4, X5, X3)) → evaluatecA_out_ga(+(X1, X2), X3)

The set Q consists of the following terms:

evaluatecA_in_ga(x0)
evaluatecA_in_gg(x0, x1)
myintegercE_in_g(x0)
U47_g(x0, x1)
U41_ga(x0, x1)
U29_gg(x0, x1, x2, x3)
U30_gg(x0, x1, x2, x3, x4)
addcB_in_ggg(x0, x1, x2)
U42_ggg(x0, x1, x2, x3)
U31_gg(x0, x1, x2, x3)
U32_gg(x0, x1, x2, x3)
U33_gg(x0, x1, x2, x3, x4)
subcC_in_ggg(x0, x1, x2)
U43_ggg(x0, x1, x2, x3)
U34_gg(x0, x1, x2, x3)
U35_gg(x0, x1, x2, x3)
U36_gg(x0, x1, x2, x3, x4)
multcD_in_gga(x0, x1)
U44_gga(x0, x1, x2)
addcF_in_gga(x0, x1)
U46_gga(x0, x1, x2)
U45_gga(x0, x1, x2)
U37_gg(x0, x1, x2, x3, x4)
U38_gg(x0, x1, x2, x3)
U41_gg(x0, x1)
U39_gg(x0, x1, x2)
U40_gg(x0, x1, x2)
U39_ga(x0, x1, x2)
U40_ga(x0, x1, x2)
U35_ga(x0, x1, x2)
U36_ga(x0, x1, x2, x3)
U37_ga(x0, x1, x2, x3)
addcB_in_gga(x0, x1)
U42_gga(x0, x1, x2)
U38_ga(x0, x1, x2)
U32_ga(x0, x1, x2)
U33_ga(x0, x1, x2, x3)
subcC_in_gga(x0, x1)
U43_gga(x0, x1, x2)
U34_ga(x0, x1, x2)
U29_ga(x0, x1, x2)
U30_ga(x0, x1, x2, x3)
U31_ga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(45) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U2_GA(X1, X2, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2)
    The graph contains the following edges 2 >= 1

  • EVALUATEA_IN_GA(+(X1, X2)) → U2_GA(X1, X2, evaluatecA_in_ga(X1))
    The graph contains the following edges 1 > 1, 1 > 2

  • U7_GA(X1, X2, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2)
    The graph contains the following edges 2 >= 1

  • U12_GA(X1, X2, evaluatecA_out_ga(X1, X4)) → EVALUATEA_IN_GA(X2)
    The graph contains the following edges 2 >= 1

  • EVALUATEA_IN_GA(-(X1, X2)) → U7_GA(X1, X2, evaluatecA_in_ga(X1))
    The graph contains the following edges 1 > 1, 1 > 2

  • EVALUATEA_IN_GA(*(X1, X2)) → U12_GA(X1, X2, evaluatecA_in_ga(X1))
    The graph contains the following edges 1 > 1, 1 > 2

  • EVALUATEA_IN_GA(+(X1, X2)) → EVALUATEA_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • EVALUATEA_IN_GA(-(X1, X2)) → EVALUATEA_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • EVALUATEA_IN_GA(*(X1, X2)) → EVALUATEA_IN_GA(X1)
    The graph contains the following edges 1 > 1

(46) YES